T:Type, x:T, L:(T List). [x / L]  []  False 

latex

Definitions	t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x), Y, ||as||, False,
Lemmas	false wf, sublist wf, non neg length, length sublist